
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Common.Utils.Names</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Common.Utils.Names" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Common.Utils.Names</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="Names">Names</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Local</span> <span class="kwd">Open</span> <span class="kwd">Scope</span> <span class="id">string</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Names.ScopedNames">ScopedNames</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="local_name">local_name</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="namespace_name">namespace_name</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="namespace_prefix">namespace_prefix</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="relative_name">relative_name</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_prefix">namespace_prefix</a></span> * <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_name">local_name</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="absolute_name">absolute_name</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="absolute_name_of_local_name">absolute_name_of_local_name</a></span> (<span class="id">ns</span>: <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>) (<span class="id">ln</span>: <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_name">local_name</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#ns">ns</a></span> ++ "." ++ <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#ln">ln</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="absolute_name_of_relative_name">absolute_name_of_relative_name</a></span> (<span class="id">local_ns</span>: <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>) (<span class="id">rn</span>: <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#relative_name">relative_name</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#rn">rn</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span>,<span class="id">ln</span>) =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_ns">local_ns</a></span> <span class="id">ln</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">ns</span>,<span class="id">ln</span>) =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name_of_local_name">absolute_name_of_local_name</a></span> <span class="id">ns</span> <span class="id">ln</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#Names.ScopedNames">ScopedNames</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Names.ReservedNames">ReservedNames</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="clause_main_name">clause_main_name</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_name">local_name</a></span> := "<span class="id">main</span>". <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="clause_init_name">clause_init_name</a></span> : <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#local_name">local_name</a></span> := "<span class="id">init</span>". <br/>
<br/>
<div class="doc">This </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="this_contract">this_contract</a></span> := "<span class="id">contract</span>". <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="this_state">this_state</a></span> := "<span class="id">state</span>".       <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="this_emit">this_emit</a></span> := "<span class="id">emit</span>".         <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="this_response">this_response</a></span> := "<span class="id">response</span>". <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="local_state">local_state</a></span> := "<span class="id">lstate</span>".     <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="local_emit">local_emit</a></span> := "<span class="id">lemit</span>".       <br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="current_time">current_time</a></span> := "<span class="id">now</span>".       <br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#Names.ReservedNames">ReservedNames</a></span>.<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Names.TypeNames">TypeNames</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="hyperledger_namespace">hyperledger_namespace</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> := "<span class="id">org.hyperledger.composer.system</span>"%<span class="id">string</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="stdlib_namespace">stdlib_namespace</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> := "<span class="id">org.accordproject.ergo.stdlib</span>"%<span class="id">string</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="default_request_absolute_name">default_request_absolute_name</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> := "<span class="id">org.accordproject.cicero.runtime.Request</span>".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="default_response_absolute_name">default_response_absolute_name</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> := "<span class="id">org.accordproject.cicero.runtime.Response</span>".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="default_emits_absolute_name">default_emits_absolute_name</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> := "<span class="id">org.hyperledger.composer.system.Event</span>".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="default_state_absolute_name">default_state_absolute_name</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> := "<span class="id">org.accordproject.cicero.contract.AccordContractState</span>".<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="default_error_absolute_name">default_error_absolute_name</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> := "<span class="id">org.accordproject.ergo.stdlib.ErgoErrorResponse</span>".<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#Names.TypeNames">TypeNames</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Names.Misc">Misc</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="function_name_in_table">function_name_in_table</a></span> (<span class="id">tname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) (<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#tname">tname</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#fname">fname</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">tname</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#tname">tname</a></span> ++ "<span class="id">_</span>" ++ <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#fname">fname</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#Names.Misc">Misc</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="Names.Namespaces">Namespaces</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="no_namespace">no_namespace</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> := "".<br/>
&nbsp;&nbsp;<span class="kwd">End</span>  <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#Names.Namespaces">Namespaces</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html#Names">Names</a></span>.<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
